YES 1.676 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((lookup :: Eq a => a  ->  [(a,b)]  ->  Maybe b) :: Eq a => a  ->  [(a,b)]  ->  Maybe b)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((lookup :: Eq b => b  ->  [(b,a)]  ->  Maybe a) :: Eq b => b  ->  [(b,a)]  ->  Maybe a)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
lookup k [] = Nothing
lookup k ((x,y: xys)
 | k == x
 = Just y
 | otherwise
 = lookup k xys

is transformed to
lookup k [] = lookup3 k []
lookup k ((x,y: xys) = lookup2 k ((x,y: xys)

lookup0 k x y xys True = lookup k xys

lookup1 k x y xys True = Just y
lookup1 k x y xys False = lookup0 k x y xys otherwise

lookup2 k ((x,y: xys) = lookup1 k x y xys (k == x)

lookup3 k [] = Nothing
lookup3 xy xz = lookup2 xy xz



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (lookup :: Eq a => a  ->  [(a,b)]  ->  Maybe b)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yu2900), Succ(yu4001000)) → new_primPlusNat(yu2900, yu4001000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yu3100), Succ(yu400100)) → new_primMulNat(yu3100, Succ(yu400100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(yu300), Succ(yu40000)) → new_primEqNat(yu300, yu40000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs(@2(yu30, yu31), @2(yu4000, yu4001), app(app(ty_@2, cc), cd), ce) → new_esEs(yu30, yu4000, cc, cd)
new_esEs(@2(yu30, yu31), @2(yu4000, yu4001), app(ty_[], cf), ce) → new_esEs0(yu30, yu4000, cf)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), gb, app(ty_Maybe, baa), hg) → new_esEs1(yu31, yu4001, baa)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), app(ty_Maybe, bbb), gc, hg) → new_esEs1(yu30, yu4000, bbb)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), app(app(app(ty_@3, bbc), bbd), bbe), gc, hg) → new_esEs2(yu30, yu4000, bbc, bbd, bbe)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), gb, gc, app(ty_[], gf)) → new_esEs0(yu32, yu4002, gf)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), gb, app(app(ty_Either, bae), baf), hg) → new_esEs3(yu31, yu4001, bae, baf)
new_esEs3(Left(yu30), Left(yu4000), app(ty_Maybe, bcd), bcb) → new_esEs1(yu30, yu4000, bcd)
new_esEs0(:(yu30, yu31), :(yu4000, yu4001), app(app(app(ty_@3, ec), ed), ee)) → new_esEs2(yu30, yu4000, ec, ed, ee)
new_esEs1(Just(yu30), Just(yu4000), app(app(ty_@2, eh), fa)) → new_esEs(yu30, yu4000, eh, fa)
new_esEs3(Right(yu30), Right(yu4000), bdb, app(app(ty_Either, beb), bec)) → new_esEs3(yu30, yu4000, beb, bec)
new_esEs(@2(yu30, yu31), @2(yu4000, yu4001), ba, app(ty_Maybe, be)) → new_esEs1(yu31, yu4001, be)
new_esEs1(Just(yu30), Just(yu4000), app(ty_[], fb)) → new_esEs0(yu30, yu4000, fb)
new_esEs3(Left(yu30), Left(yu4000), app(app(ty_Either, bch), bda), bcb) → new_esEs3(yu30, yu4000, bch, bda)
new_esEs3(Left(yu30), Left(yu4000), app(app(ty_@2, bbh), bca), bcb) → new_esEs(yu30, yu4000, bbh, bca)
new_esEs0(:(yu30, yu31), :(yu4000, yu4001), app(app(ty_Either, ef), eg)) → new_esEs3(yu30, yu4000, ef, eg)
new_esEs1(Just(yu30), Just(yu4000), app(app(ty_Either, fh), ga)) → new_esEs3(yu30, yu4000, fh, ga)
new_esEs(@2(yu30, yu31), @2(yu4000, yu4001), ba, app(app(app(ty_@3, bf), bg), bh)) → new_esEs2(yu31, yu4001, bf, bg, bh)
new_esEs(@2(yu30, yu31), @2(yu4000, yu4001), app(app(ty_Either, dd), de), ce) → new_esEs3(yu30, yu4000, dd, de)
new_esEs0(:(yu30, yu31), :(yu4000, yu4001), app(ty_Maybe, eb)) → new_esEs1(yu30, yu4000, eb)
new_esEs3(Left(yu30), Left(yu4000), app(ty_[], bcc), bcb) → new_esEs0(yu30, yu4000, bcc)
new_esEs(@2(yu30, yu31), @2(yu4000, yu4001), ba, app(app(ty_Either, ca), cb)) → new_esEs3(yu31, yu4001, ca, cb)
new_esEs3(Right(yu30), Right(yu4000), bdb, app(ty_[], bde)) → new_esEs0(yu30, yu4000, bde)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), app(app(ty_Either, bbf), bbg), gc, hg) → new_esEs3(yu30, yu4000, bbf, bbg)
new_esEs3(Right(yu30), Right(yu4000), bdb, app(ty_Maybe, bdf)) → new_esEs1(yu30, yu4000, bdf)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), gb, app(app(app(ty_@3, bab), bac), bad), hg) → new_esEs2(yu31, yu4001, bab, bac, bad)
new_esEs(@2(yu30, yu31), @2(yu4000, yu4001), ba, app(ty_[], bd)) → new_esEs0(yu31, yu4001, bd)
new_esEs1(Just(yu30), Just(yu4000), app(ty_Maybe, fc)) → new_esEs1(yu30, yu4000, fc)
new_esEs3(Right(yu30), Right(yu4000), bdb, app(app(app(ty_@3, bdg), bdh), bea)) → new_esEs2(yu30, yu4000, bdg, bdh, bea)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), gb, gc, app(ty_Maybe, gg)) → new_esEs1(yu32, yu4002, gg)
new_esEs(@2(yu30, yu31), @2(yu4000, yu4001), ba, app(app(ty_@2, bb), bc)) → new_esEs(yu31, yu4001, bb, bc)
new_esEs1(Just(yu30), Just(yu4000), app(app(app(ty_@3, fd), ff), fg)) → new_esEs2(yu30, yu4000, fd, ff, fg)
new_esEs(@2(yu30, yu31), @2(yu4000, yu4001), app(app(app(ty_@3, da), db), dc), ce) → new_esEs2(yu30, yu4000, da, db, dc)
new_esEs0(:(yu30, yu31), :(yu4000, yu4001), app(app(ty_@2, dg), dh)) → new_esEs(yu30, yu4000, dg, dh)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), gb, app(app(ty_@2, he), hf), hg) → new_esEs(yu31, yu4001, he, hf)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), app(app(ty_@2, bag), bah), gc, hg) → new_esEs(yu30, yu4000, bag, bah)
new_esEs0(:(yu30, yu31), :(yu4000, yu4001), app(ty_[], ea)) → new_esEs0(yu30, yu4000, ea)
new_esEs3(Left(yu30), Left(yu4000), app(app(app(ty_@3, bce), bcf), bcg), bcb) → new_esEs2(yu30, yu4000, bce, bcf, bcg)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), gb, gc, app(app(ty_Either, hc), hd)) → new_esEs3(yu32, yu4002, hc, hd)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), gb, gc, app(app(ty_@2, gd), ge)) → new_esEs(yu32, yu4002, gd, ge)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), app(ty_[], bba), gc, hg) → new_esEs0(yu30, yu4000, bba)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), gb, app(ty_[], hh), hg) → new_esEs0(yu31, yu4001, hh)
new_esEs2(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), gb, gc, app(app(app(ty_@3, gh), ha), hb)) → new_esEs2(yu32, yu4002, gh, ha, hb)
new_esEs0(:(yu30, yu31), :(yu4000, yu4001), df) → new_esEs0(yu31, yu4001, df)
new_esEs3(Right(yu30), Right(yu4000), bdb, app(app(ty_@2, bdc), bdd)) → new_esEs(yu30, yu4000, bdc, bdd)
new_esEs(@2(yu30, yu31), @2(yu4000, yu4001), app(ty_Maybe, cg), ce) → new_esEs1(yu30, yu4000, cg)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_lookup(yu3, :(@2(yu400, yu401), yu41), bc, bd) → new_lookup1(yu3, yu400, yu401, yu41, new_esEs4(yu3, yu400, bd), bc, bd)
new_lookup1(yu11, yu12, yu13, yu14, False, ba, bb) → new_lookup(yu11, yu14, ba, bb)

The TRS R consists of the following rules:

new_esEs21(Right(yu30), Right(yu4000), hd, ty_Char) → new_esEs20(yu30, yu4000)
new_esEs8(yu30, yu4000, app(app(app(ty_@3, fb), fc), fd)) → new_esEs5(yu30, yu4000, fb, fc, fd)
new_esEs21(Right(yu30), Right(yu4000), hd, app(app(ty_Either, bae), baf)) → new_esEs21(yu30, yu4000, bae, baf)
new_esEs6(yu32, yu4002, ty_Integer) → new_esEs10(yu32, yu4002)
new_esEs21(Left(yu30), Right(yu4000), hd, gc) → False
new_esEs21(Right(yu30), Left(yu4000), hd, gc) → False
new_esEs5(@3(yu30, yu31, yu32), @3(yu4000, yu4001, yu4002), be, bf, bg) → new_asAs(new_esEs8(yu30, yu4000, be), new_asAs(new_esEs7(yu31, yu4001, bf), new_esEs6(yu32, yu4002, bg)))
new_esEs26(yu30, yu4000, ty_Bool) → new_esEs18(yu30, yu4000)
new_primEqInt(Pos(Succ(yu300)), Neg(yu4000)) → False
new_primEqInt(Neg(Succ(yu300)), Pos(yu4000)) → False
new_esEs21(Right(yu30), Right(yu4000), hd, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs24(yu31, yu4001, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs5(yu31, yu4001, bbf, bbg, bbh)
new_esEs13([], [], bde) → True
new_esEs24(yu31, yu4001, app(ty_[], bbc)) → new_esEs13(yu31, yu4001, bbc)
new_primEqInt(Pos(Zero), Neg(Succ(yu40000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu40000))) → False
new_esEs24(yu31, yu4001, ty_Ordering) → new_esEs12(yu31, yu4001)
new_esEs8(yu30, yu4000, ty_Float) → new_esEs19(yu30, yu4000)
new_esEs21(Right(yu30), Right(yu4000), hd, ty_Ordering) → new_esEs12(yu30, yu4000)
new_esEs6(yu32, yu4002, ty_Bool) → new_esEs18(yu32, yu4002)
new_esEs15(Just(yu30), Just(yu4000), app(app(app(ty_@3, bff), bfg), bfh)) → new_esEs5(yu30, yu4000, bff, bfg, bfh)
new_esEs20(Char(yu30), Char(yu4000)) → new_primEqNat0(yu30, yu4000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs25(yu30, yu4000, ty_Char) → new_esEs20(yu30, yu4000)
new_esEs21(Left(yu30), Left(yu4000), ty_Int, gc) → new_esEs16(yu30, yu4000)
new_esEs4(yu3, yu400, ty_Float) → new_esEs19(yu3, yu400)
new_esEs8(yu30, yu4000, ty_Double) → new_esEs17(yu30, yu4000)
new_esEs15(Just(yu30), Just(yu4000), ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs15(Just(yu30), Just(yu4000), app(app(ty_Either, bga), bgb)) → new_esEs21(yu30, yu4000, bga, bgb)
new_esEs26(yu30, yu4000, app(ty_Maybe, beb)) → new_esEs15(yu30, yu4000, beb)
new_esEs6(yu32, yu4002, ty_@0) → new_esEs11(yu32, yu4002)
new_esEs24(yu31, yu4001, ty_Float) → new_esEs19(yu31, yu4001)
new_esEs26(yu30, yu4000, app(ty_Ratio, bea)) → new_esEs14(yu30, yu4000, bea)
new_esEs12(EQ, GT) → False
new_esEs12(GT, EQ) → False
new_esEs6(yu32, yu4002, ty_Float) → new_esEs19(yu32, yu4002)
new_esEs4(yu3, yu400, ty_Ordering) → new_esEs12(yu3, yu400)
new_esEs21(Right(yu30), Right(yu4000), hd, app(ty_Maybe, baa)) → new_esEs15(yu30, yu4000, baa)
new_esEs6(yu32, yu4002, app(app(app(ty_@3, ce), cf), cg)) → new_esEs5(yu32, yu4002, ce, cf, cg)
new_esEs7(yu31, yu4001, app(app(app(ty_@3, dh), ea), eb)) → new_esEs5(yu31, yu4001, dh, ea, eb)
new_esEs21(Left(yu30), Left(yu4000), app(app(app(ty_@3, gg), gh), ha), gc) → new_esEs5(yu30, yu4000, gg, gh, ha)
new_esEs6(yu32, yu4002, ty_Int) → new_esEs16(yu32, yu4002)
new_esEs25(yu30, yu4000, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs4(yu3, yu400, ty_@0) → new_esEs11(yu3, yu400)
new_sr(Neg(yu310), Pos(yu40010)) → Neg(new_primMulNat0(yu310, yu40010))
new_sr(Pos(yu310), Neg(yu40010)) → Neg(new_primMulNat0(yu310, yu40010))
new_esEs21(Right(yu30), Right(yu4000), hd, ty_Double) → new_esEs17(yu30, yu4000)
new_esEs8(yu30, yu4000, app(app(ty_Either, ff), fg)) → new_esEs21(yu30, yu4000, ff, fg)
new_esEs15(Just(yu30), Just(yu4000), ty_Int) → new_esEs16(yu30, yu4000)
new_esEs7(yu31, yu4001, ty_Float) → new_esEs19(yu31, yu4001)
new_esEs21(Right(yu30), Right(yu4000), hd, ty_Bool) → new_esEs18(yu30, yu4000)
new_esEs12(LT, GT) → False
new_esEs12(GT, LT) → False
new_esEs24(yu31, yu4001, app(ty_Maybe, bbe)) → new_esEs15(yu31, yu4001, bbe)
new_esEs13(:(yu30, yu31), :(yu4000, yu4001), bde) → new_asAs(new_esEs26(yu30, yu4000, bde), new_esEs13(yu31, yu4001, bde))
new_esEs21(Right(yu30), Right(yu4000), hd, app(ty_Ratio, hh)) → new_esEs14(yu30, yu4000, hh)
new_esEs8(yu30, yu4000, app(app(ty_@2, ee), ef)) → new_esEs9(yu30, yu4000, ee, ef)
new_esEs21(Left(yu30), Left(yu4000), ty_Double, gc) → new_esEs17(yu30, yu4000)
new_esEs21(Right(yu30), Right(yu4000), hd, app(ty_[], hg)) → new_esEs13(yu30, yu4000, hg)
new_esEs21(Left(yu30), Left(yu4000), ty_Integer, gc) → new_esEs10(yu30, yu4000)
new_esEs23(yu30, yu4000, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs7(yu31, yu4001, app(app(ty_Either, ec), ed)) → new_esEs21(yu31, yu4001, ec, ed)
new_esEs15(Just(yu30), Just(yu4000), ty_@0) → new_esEs11(yu30, yu4000)
new_esEs6(yu32, yu4002, ty_Char) → new_esEs20(yu32, yu4002)
new_esEs7(yu31, yu4001, ty_Char) → new_esEs20(yu31, yu4001)
new_esEs22(yu31, yu4001, ty_Integer) → new_esEs10(yu31, yu4001)
new_primEqNat0(Succ(yu300), Zero) → False
new_primEqNat0(Zero, Succ(yu40000)) → False
new_esEs4(yu3, yu400, app(ty_Ratio, fh)) → new_esEs14(yu3, yu400, fh)
new_primPlusNat0(Zero, Zero) → Zero
new_esEs21(Right(yu30), Right(yu4000), hd, ty_@0) → new_esEs11(yu30, yu4000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs24(yu31, yu4001, app(ty_Ratio, bbd)) → new_esEs14(yu31, yu4001, bbd)
new_esEs10(Integer(yu30), Integer(yu4000)) → new_primEqInt(yu30, yu4000)
new_esEs14(:%(yu30, yu31), :%(yu4000, yu4001), fh) → new_asAs(new_esEs23(yu30, yu4000, fh), new_esEs22(yu31, yu4001, fh))
new_esEs17(Double(yu30, yu31), Double(yu4000, yu4001)) → new_esEs16(new_sr(yu30, yu4000), new_sr(yu31, yu4001))
new_esEs11(@0, @0) → True
new_esEs25(yu30, yu4000, ty_@0) → new_esEs11(yu30, yu4000)
new_esEs7(yu31, yu4001, ty_Integer) → new_esEs10(yu31, yu4001)
new_esEs15(Nothing, Nothing, beh) → True
new_esEs26(yu30, yu4000, ty_Int) → new_esEs16(yu30, yu4000)
new_esEs7(yu31, yu4001, ty_@0) → new_esEs11(yu31, yu4001)
new_primPlusNat1(Succ(yu290), yu400100) → Succ(Succ(new_primPlusNat0(yu290, yu400100)))
new_esEs24(yu31, yu4001, ty_@0) → new_esEs11(yu31, yu4001)
new_esEs15(Just(yu30), Just(yu4000), app(app(ty_@2, bfa), bfb)) → new_esEs9(yu30, yu4000, bfa, bfb)
new_esEs25(yu30, yu4000, ty_Int) → new_esEs16(yu30, yu4000)
new_esEs8(yu30, yu4000, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs15(Just(yu30), Just(yu4000), app(ty_[], bfc)) → new_esEs13(yu30, yu4000, bfc)
new_esEs25(yu30, yu4000, app(ty_Ratio, bcf)) → new_esEs14(yu30, yu4000, bcf)
new_esEs26(yu30, yu4000, ty_Double) → new_esEs17(yu30, yu4000)
new_esEs8(yu30, yu4000, app(ty_[], eg)) → new_esEs13(yu30, yu4000, eg)
new_esEs26(yu30, yu4000, ty_Char) → new_esEs20(yu30, yu4000)
new_esEs21(Left(yu30), Left(yu4000), app(app(ty_Either, hb), hc), gc) → new_esEs21(yu30, yu4000, hb, hc)
new_esEs25(yu30, yu4000, ty_Double) → new_esEs17(yu30, yu4000)
new_sr(Neg(yu310), Neg(yu40010)) → Pos(new_primMulNat0(yu310, yu40010))
new_esEs12(LT, LT) → True
new_esEs15(Just(yu30), Just(yu4000), ty_Double) → new_esEs17(yu30, yu4000)
new_esEs15(Just(yu30), Just(yu4000), app(ty_Ratio, bfd)) → new_esEs14(yu30, yu4000, bfd)
new_sr(Pos(yu310), Pos(yu40010)) → Pos(new_primMulNat0(yu310, yu40010))
new_asAs(False, yu28) → False
new_esEs7(yu31, yu4001, ty_Bool) → new_esEs18(yu31, yu4001)
new_esEs24(yu31, yu4001, ty_Int) → new_esEs16(yu31, yu4001)
new_primEqNat0(Zero, Zero) → True
new_esEs8(yu30, yu4000, ty_Char) → new_esEs20(yu30, yu4000)
new_esEs13([], :(yu4000, yu4001), bde) → False
new_esEs13(:(yu30, yu31), [], bde) → False
new_primMulNat0(Succ(yu3100), Zero) → Zero
new_primMulNat0(Zero, Succ(yu400100)) → Zero
new_primMulNat0(Succ(yu3100), Succ(yu400100)) → new_primPlusNat1(new_primMulNat0(yu3100, Succ(yu400100)), yu400100)
new_esEs26(yu30, yu4000, app(app(ty_@2, bdf), bdg)) → new_esEs9(yu30, yu4000, bdf, bdg)
new_esEs25(yu30, yu4000, ty_Bool) → new_esEs18(yu30, yu4000)
new_esEs6(yu32, yu4002, app(app(ty_Either, da), db)) → new_esEs21(yu32, yu4002, da, db)
new_esEs18(True, True) → True
new_esEs6(yu32, yu4002, app(ty_[], cb)) → new_esEs13(yu32, yu4002, cb)
new_esEs4(yu3, yu400, ty_Int) → new_esEs16(yu3, yu400)
new_esEs6(yu32, yu4002, ty_Ordering) → new_esEs12(yu32, yu4002)
new_esEs21(Left(yu30), Left(yu4000), app(ty_Maybe, gf), gc) → new_esEs15(yu30, yu4000, gf)
new_esEs21(Left(yu30), Left(yu4000), ty_Ordering, gc) → new_esEs12(yu30, yu4000)
new_esEs4(yu3, yu400, app(ty_Maybe, beh)) → new_esEs15(yu3, yu400, beh)
new_esEs4(yu3, yu400, app(app(app(ty_@3, be), bf), bg)) → new_esEs5(yu3, yu400, be, bf, bg)
new_esEs21(Right(yu30), Right(yu4000), hd, ty_Int) → new_esEs16(yu30, yu4000)
new_esEs24(yu31, yu4001, ty_Char) → new_esEs20(yu31, yu4001)
new_esEs25(yu30, yu4000, app(ty_Maybe, bcg)) → new_esEs15(yu30, yu4000, bcg)
new_esEs7(yu31, yu4001, ty_Ordering) → new_esEs12(yu31, yu4001)
new_esEs21(Left(yu30), Left(yu4000), app(ty_Ratio, ge), gc) → new_esEs14(yu30, yu4000, ge)
new_esEs8(yu30, yu4000, ty_Int) → new_esEs16(yu30, yu4000)
new_esEs25(yu30, yu4000, app(ty_[], bce)) → new_esEs13(yu30, yu4000, bce)
new_esEs24(yu31, yu4001, ty_Integer) → new_esEs10(yu31, yu4001)
new_esEs26(yu30, yu4000, app(app(ty_Either, bef), beg)) → new_esEs21(yu30, yu4000, bef, beg)
new_esEs21(Right(yu30), Right(yu4000), hd, ty_Float) → new_esEs19(yu30, yu4000)
new_esEs23(yu30, yu4000, ty_Int) → new_esEs16(yu30, yu4000)
new_esEs25(yu30, yu4000, app(app(ty_@2, bcc), bcd)) → new_esEs9(yu30, yu4000, bcc, bcd)
new_esEs24(yu31, yu4001, ty_Double) → new_esEs17(yu31, yu4001)
new_esEs21(Right(yu30), Right(yu4000), hd, app(app(app(ty_@3, bab), bac), bad)) → new_esEs5(yu30, yu4000, bab, bac, bad)
new_esEs4(yu3, yu400, ty_Bool) → new_esEs18(yu3, yu400)
new_esEs4(yu3, yu400, ty_Integer) → new_esEs10(yu3, yu400)
new_esEs15(Just(yu30), Just(yu4000), ty_Float) → new_esEs19(yu30, yu4000)
new_esEs25(yu30, yu4000, ty_Ordering) → new_esEs12(yu30, yu4000)
new_esEs7(yu31, yu4001, ty_Int) → new_esEs16(yu31, yu4001)
new_primEqInt(Neg(Succ(yu300)), Neg(Succ(yu40000))) → new_primEqNat0(yu300, yu40000)
new_esEs24(yu31, yu4001, ty_Bool) → new_esEs18(yu31, yu4001)
new_esEs4(yu3, yu400, ty_Double) → new_esEs17(yu3, yu400)
new_esEs25(yu30, yu4000, ty_Float) → new_esEs19(yu30, yu4000)
new_esEs21(Left(yu30), Left(yu4000), ty_Float, gc) → new_esEs19(yu30, yu4000)
new_esEs4(yu3, yu400, app(app(ty_Either, hd), gc)) → new_esEs21(yu3, yu400, hd, gc)
new_esEs26(yu30, yu4000, app(ty_[], bdh)) → new_esEs13(yu30, yu4000, bdh)
new_esEs15(Just(yu30), Just(yu4000), ty_Ordering) → new_esEs12(yu30, yu4000)
new_esEs7(yu31, yu4001, app(ty_Maybe, dg)) → new_esEs15(yu31, yu4001, dg)
new_esEs15(Just(yu30), Just(yu4000), app(ty_Maybe, bfe)) → new_esEs15(yu30, yu4000, bfe)
new_esEs8(yu30, yu4000, app(ty_Ratio, eh)) → new_esEs14(yu30, yu4000, eh)
new_esEs16(yu3, yu400) → new_primEqInt(yu3, yu400)
new_esEs12(LT, EQ) → False
new_esEs12(EQ, LT) → False
new_esEs7(yu31, yu4001, app(ty_[], de)) → new_esEs13(yu31, yu4001, de)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs25(yu30, yu4000, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs5(yu30, yu4000, bch, bda, bdb)
new_esEs21(Left(yu30), Left(yu4000), ty_Char, gc) → new_esEs20(yu30, yu4000)
new_esEs26(yu30, yu4000, ty_Float) → new_esEs19(yu30, yu4000)
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_esEs6(yu32, yu4002, app(app(ty_@2, bh), ca)) → new_esEs9(yu32, yu4002, bh, ca)
new_esEs12(GT, GT) → True
new_esEs7(yu31, yu4001, app(app(ty_@2, dc), dd)) → new_esEs9(yu31, yu4001, dc, dd)
new_primEqInt(Neg(Succ(yu300)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu40000))) → False
new_esEs19(Float(yu30, yu31), Float(yu4000, yu4001)) → new_esEs16(new_sr(yu30, yu4000), new_sr(yu31, yu4001))
new_esEs21(Left(yu30), Left(yu4000), ty_@0, gc) → new_esEs11(yu30, yu4000)
new_primPlusNat1(Zero, yu400100) → Succ(yu400100)
new_esEs24(yu31, yu4001, app(app(ty_@2, bba), bbb)) → new_esEs9(yu31, yu4001, bba, bbb)
new_esEs15(Just(yu30), Just(yu4000), ty_Char) → new_esEs20(yu30, yu4000)
new_primPlusNat0(Succ(yu2900), Succ(yu4001000)) → Succ(Succ(new_primPlusNat0(yu2900, yu4001000)))
new_esEs21(Left(yu30), Left(yu4000), app(ty_[], gd), gc) → new_esEs13(yu30, yu4000, gd)
new_esEs26(yu30, yu4000, ty_@0) → new_esEs11(yu30, yu4000)
new_esEs21(Right(yu30), Right(yu4000), hd, app(app(ty_@2, he), hf)) → new_esEs9(yu30, yu4000, he, hf)
new_esEs15(Just(yu30), Just(yu4000), ty_Bool) → new_esEs18(yu30, yu4000)
new_asAs(True, yu28) → yu28
new_esEs26(yu30, yu4000, app(app(app(ty_@3, bec), bed), bee)) → new_esEs5(yu30, yu4000, bec, bed, bee)
new_esEs15(Just(yu30), Nothing, beh) → False
new_esEs15(Nothing, Just(yu4000), beh) → False
new_esEs6(yu32, yu4002, app(ty_Ratio, cc)) → new_esEs14(yu32, yu4002, cc)
new_esEs6(yu32, yu4002, ty_Double) → new_esEs17(yu32, yu4002)
new_esEs4(yu3, yu400, app(app(ty_@2, bag), bah)) → new_esEs9(yu3, yu400, bag, bah)
new_esEs8(yu30, yu4000, ty_@0) → new_esEs11(yu30, yu4000)
new_primEqInt(Pos(Succ(yu300)), Pos(Succ(yu40000))) → new_primEqNat0(yu300, yu40000)
new_esEs26(yu30, yu4000, ty_Integer) → new_esEs10(yu30, yu4000)
new_esEs4(yu3, yu400, app(ty_[], bde)) → new_esEs13(yu3, yu400, bde)
new_esEs8(yu30, yu4000, ty_Ordering) → new_esEs12(yu30, yu4000)
new_esEs7(yu31, yu4001, app(ty_Ratio, df)) → new_esEs14(yu31, yu4001, df)
new_esEs25(yu30, yu4000, app(app(ty_Either, bdc), bdd)) → new_esEs21(yu30, yu4000, bdc, bdd)
new_esEs6(yu32, yu4002, app(ty_Maybe, cd)) → new_esEs15(yu32, yu4002, cd)
new_esEs9(@2(yu30, yu31), @2(yu4000, yu4001), bag, bah) → new_asAs(new_esEs25(yu30, yu4000, bag), new_esEs24(yu31, yu4001, bah))
new_primEqNat0(Succ(yu300), Succ(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs26(yu30, yu4000, ty_Ordering) → new_esEs12(yu30, yu4000)
new_esEs21(Left(yu30), Left(yu4000), app(app(ty_@2, ga), gb), gc) → new_esEs9(yu30, yu4000, ga, gb)
new_esEs8(yu30, yu4000, ty_Bool) → new_esEs18(yu30, yu4000)
new_esEs21(Left(yu30), Left(yu4000), ty_Bool, gc) → new_esEs18(yu30, yu4000)
new_esEs24(yu31, yu4001, app(app(ty_Either, bca), bcb)) → new_esEs21(yu31, yu4001, bca, bcb)
new_esEs12(EQ, EQ) → True
new_primEqInt(Pos(Succ(yu300)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(yu40000))) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs4(yu3, yu400, ty_Char) → new_esEs20(yu3, yu400)
new_primPlusNat0(Zero, Succ(yu4001000)) → Succ(yu4001000)
new_primPlusNat0(Succ(yu2900), Zero) → Succ(yu2900)
new_esEs22(yu31, yu4001, ty_Int) → new_esEs16(yu31, yu4001)
new_esEs8(yu30, yu4000, app(ty_Maybe, fa)) → new_esEs15(yu30, yu4000, fa)
new_esEs18(False, False) → True
new_esEs7(yu31, yu4001, ty_Double) → new_esEs17(yu31, yu4001)

The set Q consists of the following terms:

new_esEs21(Left(x0), Left(x1), ty_Bool, x2)
new_esEs21(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs15(Just(x0), Just(x1), ty_Char)
new_esEs6(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs15(Just(x0), Just(x1), ty_@0)
new_esEs15(Nothing, Nothing, x0)
new_esEs26(x0, x1, ty_Char)
new_esEs7(x0, x1, ty_Bool)
new_esEs8(x0, x1, ty_Integer)
new_esEs8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13([], :(x0, x1), x2)
new_esEs15(Just(x0), Nothing, x1)
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Int)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs18(False, True)
new_esEs18(True, False)
new_esEs4(x0, x1, ty_Ordering)
new_esEs15(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs15(Just(x0), Just(x1), ty_Float)
new_esEs9(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs21(Right(x0), Right(x1), x2, ty_Int)
new_esEs21(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs4(x0, x1, ty_Char)
new_esEs7(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs15(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs21(Left(x0), Left(x1), ty_Double, x2)
new_esEs8(x0, x1, app(ty_[], x2))
new_esEs8(x0, x1, ty_Bool)
new_esEs11(@0, @0)
new_esEs21(Left(x0), Left(x1), ty_Int, x2)
new_esEs24(x0, x1, ty_Float)
new_primPlusNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)
new_esEs17(Double(x0, x1), Double(x2, x3))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs21(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs13(:(x0, x1), :(x2, x3), x4)
new_esEs21(Right(x0), Right(x1), x2, ty_Float)
new_esEs6(x0, x1, app(ty_Ratio, x2))
new_esEs7(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs15(Nothing, Just(x0), x1)
new_esEs7(x0, x1, ty_Char)
new_esEs12(GT, EQ)
new_esEs12(EQ, GT)
new_esEs24(x0, x1, ty_Ordering)
new_esEs21(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs7(x0, x1, ty_Float)
new_esEs21(Right(x0), Right(x1), x2, ty_Double)
new_esEs21(Left(x0), Left(x1), ty_Float, x2)
new_esEs18(True, True)
new_esEs5(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs8(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Int)
new_esEs15(Just(x0), Just(x1), ty_Bool)
new_esEs21(Right(x0), Right(x1), x2, ty_@0)
new_esEs6(x0, x1, ty_Float)
new_esEs21(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs7(x0, x1, ty_Int)
new_esEs12(GT, GT)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs21(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs26(x0, x1, ty_@0)
new_esEs13([], [], x0)
new_esEs8(x0, x1, ty_Int)
new_esEs10(Integer(x0), Integer(x1))
new_esEs6(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primMulNat0(Zero, Succ(x0))
new_esEs24(x0, x1, ty_Bool)
new_esEs15(Just(x0), Just(x1), ty_Double)
new_esEs7(x0, x1, ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs21(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_Bool)
new_esEs7(x0, x1, ty_Double)
new_esEs6(x0, x1, ty_Int)
new_esEs15(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs15(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs15(Just(x0), Just(x1), app(ty_[], x2))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Float)
new_primEqNat0(Zero, Zero)
new_esEs25(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Integer)
new_esEs21(Right(x0), Right(x1), x2, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs21(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs7(x0, x1, ty_Ordering)
new_esEs21(Right(x0), Right(x1), x2, ty_Integer)
new_esEs26(x0, x1, ty_Double)
new_esEs6(x0, x1, ty_Ordering)
new_esEs21(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs21(Left(x0), Left(x1), ty_@0, x2)
new_esEs4(x0, x1, ty_@0)
new_esEs21(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(Char(x0), Char(x1))
new_esEs8(x0, x1, ty_Float)
new_esEs23(x0, x1, ty_Integer)
new_sr(Neg(x0), Neg(x1))
new_primMulNat0(Zero, Zero)
new_esEs6(x0, x1, app(ty_[], x2))
new_esEs15(Just(x0), Just(x1), ty_Ordering)
new_esEs21(Right(x0), Left(x1), x2, x3)
new_esEs21(Left(x0), Right(x1), x2, x3)
new_esEs25(x0, x1, ty_Bool)
new_esEs19(Float(x0, x1), Float(x2, x3))
new_esEs13(:(x0, x1), [], x2)
new_esEs21(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs15(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs8(x0, x1, ty_Char)
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs7(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(x0, x1, ty_Integer)
new_esEs6(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Double)
new_esEs6(x0, x1, ty_Char)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Double)
new_esEs8(x0, x1, app(ty_Ratio, x2))
new_esEs15(Just(x0), Just(x1), ty_Int)
new_esEs21(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Ordering)
new_esEs7(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Int)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs8(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs8(x0, x1, ty_@0)
new_esEs18(False, False)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_asAs(False, x0)
new_esEs21(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs15(Just(x0), Just(x1), ty_Integer)
new_esEs24(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs25(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Float)
new_esEs21(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs23(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Bool)
new_esEs7(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs8(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Double)
new_primPlusNat0(Succ(x0), Zero)
new_esEs12(EQ, LT)
new_esEs12(LT, EQ)
new_esEs21(Left(x0), Left(x1), ty_Integer, x2)
new_primMulNat0(Succ(x0), Zero)
new_esEs21(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs6(x0, x1, ty_@0)
new_esEs12(EQ, EQ)
new_primPlusNat0(Zero, Zero)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs7(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Zero, Succ(x0))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs8(x0, x1, app(ty_Maybe, x2))
new_esEs6(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(x0, x1)
new_esEs24(x0, x1, ty_Integer)
new_esEs6(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs12(LT, LT)
new_asAs(True, x0)
new_esEs25(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Integer)
new_esEs12(LT, GT)
new_esEs12(GT, LT)
new_esEs8(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, ty_Char)
new_primEqNat0(Succ(x0), Zero)
new_esEs24(x0, x1, ty_Int)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: